/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.winningCondition;

import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.formula.BuchiGameIterator;
import chameleon.model.formula.Formula;
import chameleon.model.formula.parser.BooleanParser;
import chameleon.model.satSolver.SatSolver;
import com.sun.jna.Pointer;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.Vector;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.TimeoutException;

/**
 * This class represent a winning condition for the game. We suppose that
 * this class recieve in paramter an LTL formula that respects the SPL
 * specification. They exists 7 kind of winning condition for NuGat :
 *  -REACHTARGET
 *  -REACHDEADLOCK
 *  -AVOIDTARGET
 *  -AVOIDDEADLOCK
 *  -BUCHIGAME
 *  -GENREACIVITYGAME
 *  -LTLGAME
 *
 * This class takes an LTL Formula on input. First analyze the LTL formula to
 * determine which kind of condition is represented. Second create the NuGat
 * corresponding condition. At the moment only REACH and AVOID property.
 *
 * @author simon
 */
public class WinningCondition {
    private NuGatInterface nugat_;
    private Formula ltlFormula_; //For create the winning condition
    private int typeProperty_;
    private int player_; //1 or 2
    private Formula exp_opt;
    private Node GenReactLeft_;
    private Node GenReactRight_;
    private Hashtable smvTable_;

    //********************* CONSTRUCTOR *********************************//

    public WinningCondition(NuGatInterface nugat){
        nugat_ = nugat;
    }
    
    public WinningCondition(NuGatInterface nugat,
            Formula wc,String player, Hashtable smvTable) throws IOException{
        ltlFormula_ = wc;
        player_ = getPlayer(player);
        nugat_ = nugat;
        smvTable_ = smvTable;
        typeProperty_ = getType(wc);
        initExpOpt(wc);
        //constructWC();
    }
    
    
    public WinningCondition(NuGatInterface nugat,
            Formula wc,int player) throws IOException{
        ltlFormula_ = wc;
        player_ = player;
        nugat_ = nugat;
        constructWC();
    }
    
    public WinningCondition(NuGatInterface nugat,
            Formula wc,int player, Hashtable smvTable) throws IOException{
        ltlFormula_ = wc;
        player_ = player;
        nugat_ = nugat;
        smvTable_ = smvTable;
        constructWC();
    }

    public WinningCondition(NuGatInterface nugat, String type,
            String player, String target){
        nugat_ = nugat;
        typeProperty_ = getType(type);
        player_ = getPlayer(player);
        if (typeProperty_ != Tag.AVOIDDEADLOCK && typeProperty_ != Tag.REACHDEADLOCK){
            BooleanParser parser;
            try {
                parser = new BooleanParser(target);
                exp_opt = parser.createFormula();
            } catch (IOException ex) {
                Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
            }
        }
    }

    /**
     * Constructor for GR(1) game
     */
    
    public WinningCondition(NuGatInterface nugat, String type, String player, String left,
            String right){
        typeProperty_ = getType(type);
        player_ = getPlayer(player);
        
    }
    
    
    private void initExpOpt(Formula expOpt) throws IOException{
    
        if (typeProperty_ == Tag.AVOIDTARGET || typeProperty_ == Tag.REACHTARGET)
             exp_opt = expOpt.getRightF();
        else if (typeProperty_ == Tag.BUCHIGAME)
            createBuchiGame();
        else if (typeProperty_ == Tag.GENREACTIVITY)
            createGR1Game();
        else
            exp_opt = expOpt;
            
        /*switch(typeProperty_){
            case Tag.AVOIDTARGET:
                    exp_opt = expOpt.getRightF();
            case Tag.REACHTARGET:
                    exp_opt = expOpt.getRightF();
            case Tag.BUCHIGAME:
                    createBuchiGame();
            case Tag.GENREACTIVITY:
                    createGR1Game();
            default:
                    exp_opt = expOpt;
        }*/
    }   
    
    
    /**
     * This method analyze the LTL formula to determine which kind of condition
     * we have. So this function initialize field :
     *  -exp_opt in function of typeProperty_
     *
     */

    private void constructWC() throws IOException {
        int operator = ltlFormula_.getOperator().getTag();

        switch (operator){
            //REACH PROPERTY
            case chameleon.model.formula.Tag.EVENTUALLY:
                    /*The input formula is F (boolean_expression) and exp_opt
                     * is just the boolean_expression.
                     */
                    exp_opt = ltlFormula_.getRightF();
                    File formula = exp_opt.getCnfFile();
                    SatSolver satSolver = new SatSolver(formula.getPath());
                    formula.deleteOnExit();
                    try {
                        if (satSolver.isSatisfiable())
                            typeProperty_ = Tag.REACHTARGET;
                        else
                            typeProperty_ = Tag.REACHDEADLOCK;
                    } catch (FileNotFoundException ex) {
                        Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
                    } catch (ParseFormatException ex) {
                        Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
                    } catch (TimeoutException ex) {
                        Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
                    } catch (ContradictionException ex) {
                        Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
                    }
                break;
            //AVOID PROPERTY
            case chameleon.model.formula.Tag.ALWAYS:
               if (ltlFormula_.getRightF().getOperator().isEquals(chameleon.model.formula.Tag.NOT)){
                   /*The input formula is G (boolean_expression) and exp_opt
                     * is just the boolean_expression.
                     */
                    exp_opt = ltlFormula_.getRightF().getRightF();
                    formula = exp_opt.getCnfFile();
                    satSolver = new SatSolver(formula.getPath());
                    try {
                        if (satSolver.isSatisfiable()) {
                            typeProperty_ = Tag.AVOIDTARGET;
                        } else {
                            typeProperty_ = Tag.AVOIDDEADLOCK;
                        }
                    } catch (FileNotFoundException ex) {
                        Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
                    } catch (ParseFormatException ex) {
                        Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
                    } catch (TimeoutException ex) {
                        Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
                    } catch (ContradictionException ex) {
                        Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
                    }
                }
               //BUCHIGAME
               else if (ltlFormula_.getRightF().getOperator().isEquals(chameleon.model.formula.Tag.EVENTUALLY))
                   createBuchiGame();
                else{
                    throw new IOException("SingleWinningCondition :: Uncorrect winning condition");
                }
                break;
            //BUCHIGAME
            case chameleon.model.formula.Tag.AND:
                createBuchiGame();
                break;
            //GENERAL REACTIVITY GAME
            case chameleon.model.formula.Tag.IMPLIES:
                if (isCorrectGR(ltlFormula_)){
                    GenReactLeft_ = createGrBuchiNode(ltlFormula_.getLeftF());
                    GenReactRight_ = createGrBuchiNode(ltlFormula_.getRightF());
                    typeProperty_ = Tag.GENREACTIVITY;
                    //exp_opt = new Formula(left, right, new Operator("->"));
                }
                else{
                    throw new IOException("SingleWinningCondition :: Uncorrect winning condition");
                }
                break;
            default:
                typeProperty_ = Tag.LTLGAME;
        }
    }
    
    private void createBuchiGame() throws IOException{
        if (isCorrectBuchiGame(ltlFormula_)){
            GenReactLeft_ = createGrBuchiNode(ltlFormula_);
            typeProperty_ = Tag.BUCHIGAME;
        }
        else{
            throw new IOException("SingleWinningCondition :: Uncorrect winning condition");
        }
    }
    
    private void createGR1Game() throws IOException{
        GenReactLeft_ = createGrBuchiNode(ltlFormula_.getLeftF());
        GenReactRight_ = createGrBuchiNode(ltlFormula_.getRightF());
    }
    
    //********************** GETTER *************************************//

    private int getType(String type){
        if (type.equals("REACHTARGET"))
            return Tag.REACHTARGET;
        else if (type.equals("REACHDEADLOCK"))
            return Tag.REACHDEADLOCK;
        else if (type.equals("AVOIDTARGET"))
            return Tag.AVOIDTARGET;
        else if (type.equals("AVOIDDEADLOCK"))
            return Tag.AVOIDDEADLOCK;
        else if (type.equals("GENREACTIVITY"))
            return Tag.GENREACTIVITY;
        else if (type.equals("BUCHIGAME"))
            return Tag.BUCHIGAME;
        else if (type.equals("LTLGAME"))
            return Tag.LTLGAME;
        else
            throw new RuntimeException("SinglWinningCondition : Unsported condition yet");
    }

    private int getType(Formula expOpt) throws IOException{
        int firstOp = expOpt.getOperator().getTag();
        int secondOp = -1;
        if (!expOpt.getRightF().isAtomic())
            secondOp = expOpt.getRightF().getOperator().getTag();
        
        if (firstOp == chameleon.model.formula.Tag.EVENTUALLY &&
                expOpt.getRightF().isSatFormula()){
            if (expOpt.getRightF().isFalse()){
                return Tag.REACHDEADLOCK;
            }
            else
                return Tag.REACHTARGET;
        }
        else if (firstOp == chameleon.model.formula.Tag.ALWAYS &&
                secondOp == chameleon.model.formula.Tag.NOT &&
                expOpt.getRightF().isSatFormula()){
            if (expOpt.getRightF().isFalse())
                return Tag.AVOIDDEADLOCK;
            else
                return Tag.AVOIDTARGET;
        }
        else if (((firstOp == chameleon.model.formula.Tag.AND ) || 
                 (firstOp ==chameleon.model.formula.Tag.ALWAYS &&
                  expOpt.getRightF().getOperator().getTag() == chameleon.model.formula.Tag.EVENTUALLY ))
                && isCorrectBuchiGame(expOpt))
            return Tag.BUCHIGAME;
        else if (firstOp == chameleon.model.formula.Tag.IMPLIES &&
                isCorrectGR(expOpt))
            return Tag.GENREACTIVITY;
        else
            return Tag.LTLGAME;
    }
    
    private int getPlayer(String player){
        if (player.equals("P1"))
            return 1;
        else if (player.equals("P2"))
            return 2;
        else
            throw new RuntimeException("SingleWinningCondition : Only two players game"
                    + "are suported");
    }

    public int getPropertyKind(){
        return typeProperty_;
    }

    public Formula getFormula(){
        return ltlFormula_;
    }

    public PropGame getPropGame(){
        return new PropGame(getExpr(), getPropGameType(),nugat_);
    }

    /**
     * This function return the corresponding tag in NuGat for the condition
     * @return
     */

    private int getPropGameType(){
        switch(typeProperty_){
            case Tag.REACHTARGET:
                return nugat_.PropGame_ReachTarget;
            case Tag.REACHDEADLOCK:
                return nugat_.PropGame_ReachDeadlock;
            case Tag.AVOIDTARGET:
                return nugat_.PropGame_AvoidTarget;
            case Tag.AVOIDDEADLOCK:
                return nugat_.PropGame_AvoidDeadlock;
            case Tag.GENREACTIVITY:
                return nugat_.PropGame_GenReactivity;
            case Tag.BUCHIGAME:
                return nugat_.PropGame_BuchiGame;
            case Tag.LTLGAME:
                return nugat_.PropGame_LtlGame;
            default:
                throw new RuntimeException("SingleWinningCondition :: Unsported condition");
        }
    }

    /**
     * This method return the corresponding NuGat expression for the present
     * condition.
     * @return node_ptr
     */

    private Node getExpr() {
        if (isReachAvoidProp() || typeProperty_ == Tag.LTLGAME)
            return new Node(nugat_.GAME_SPEC_WRAPPER, getNuGatPlayer(), getTarget().ptr(),
                nugat_);
        else if (typeProperty_ == Tag.GENREACTIVITY){
            Node exprCore = new Node (nugat_.GAME_TWO_EXP_LISTS,GenReactLeft_,
                    GenReactRight_, nugat_);
            return new Node(nugat_.GAME_SPEC_WRAPPER, getNuGatPlayer(), exprCore.ptr(),
                nugat_);
        }
        else if (typeProperty_ == Tag.BUCHIGAME){
            Node exprCore = new Node(nugat_.GAME_EXP_LIST, GenReactLeft_, 
                    new Node(Pointer.NULL,nugat_), nugat_ );
            return new Node(nugat_.GAME_SPEC_WRAPPER, getNuGatPlayer(), exprCore.ptr(),
                nugat_);
        }
        else
            throw new RuntimeException("Winning Condition :: Unsuported winning condition");
    }

    private boolean isReachAvoidProp(){
        return (typeProperty_ == Tag.REACHDEADLOCK 
                || typeProperty_ == Tag.REACHTARGET
                || typeProperty_ == Tag.AVOIDDEADLOCK
                || typeProperty_ == Tag.AVOIDTARGET);
    }
    
    /**
     * This function return the NuGat representation for a player.
     * @return
     */

    private Pointer getNuGatPlayer(){
        if (player_==1)
            return nugat_.sym_intern(nugat_.PLAYER_NAME_1);
        else if (player_==2)
            return nugat_.sym_intern(nugat_.PLAYER_NAME_2);
        else
            throw new RuntimeException("SingleWinningCondition :: Only two player games"
                    + "are supported!");
    }

    /**
     * This function convert an LTL formula to his NuGat node representation.
     * @return
     */

    private Node getTarget() {
            if (exp_opt != null)
                return exp_opt.encFormula( nugat_, smvTable_);
            else
                return new Node(Pointer.NULL,nugat_);
    }

    //********************* SETTER **************************************//

    public void setPlayer(String player){
        player_ = getPlayer(player);
    }
    
    public void setProperty(String property){
        typeProperty_ = getType(property);
    }
    
    public void setExpOpt(Formula formula){
        exp_opt = formula;
    }
    
    public void setGRleft (String formula){
        try {
            GenReactLeft_ = createGrBuchiNode(formula);
        } catch (IOException ex) {
            Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
        }
    }
    
    public void setGRRight (String formula){
        try {
            GenReactRight_ = createGrBuchiNode(formula);
        } catch (IOException ex) {
            Logger.getLogger(WinningCondition.class.getName()).log(Level.SEVERE, null, ex);
        }
    }
    
    public void setSmvTable(Hashtable smvTable){
        smvTable_ = smvTable;
    }

    private boolean isCorrectBuchiGame(Formula formula) throws IOException {
        /**
         * Structure Büchi Game : AND(GF!prop)
         * For a Buchi Game, the structure is the following :
         *  -on top we have the and operator,
         *  -on left we have an Always operator,
         *  -on right we have an and operotar or an always operator if it is
         * the end
         */
        
        int operator = formula.getOperator().getTag();
        
        if ( operator == chameleon.model.formula.Tag.ALWAYS
                && formula.getRightF().getOperator().getTag() == chameleon.model.formula.Tag.EVENTUALLY
                && formula.getRightF().getRightF().isSatFormula())
            return true;
        else if (operator == chameleon.model.formula.Tag.AND)
            return (isCorrectBuchiGame(formula.getLeftF()) 
                    && isCorrectBuchiGame(formula.getRightF()));
        else        
            return false;
    }

    private boolean isCorrectGR(Formula ltlFormula_) throws IOException {
        return (isCorrectBuchiGame(ltlFormula_.getLeftF())
                && isCorrectBuchiGame(ltlFormula_.getRightF()));
    }
    
    public Node createGrBuchiNode(String propositions) throws IOException{
        String[] param = propositions.split(",");
        Vector<Formula> paramFormula = new Vector<Formula>();
        
        for (int i = 0 ; i < param.length; ++i){
            BooleanParser parser = new BooleanParser(param[i]);
            paramFormula.add(parser.createFormula());
        }
        
        return createGrBuchiNode(formulaToNode(paramFormula));
    }
    
    private Node createGrBuchiNode(Formula formula) throws IOException {
        Vector<Formula> buchiProp = new Vector<Formula>();
        buchiProp = CompleteBuchiGame(formula);
        buchiProp = inverse(buchiProp);
        return createGrBuchiNode( formulaToNode(buchiProp));
    }
    
    private Node createGrBuchiNode(Vector<Node> buchiNodes) throws IOException {
        Node buchiNode;
        if (buchiNodes.size() == 1){
            buchiNode = new Node(nugat_.CONS, buchiNodes.get(0),
                    new Node(Pointer.NULL,nugat_),nugat_);
        }
        else{
            buchiNode = new Node(nugat_.CONS, buchiNodes.get(1),
                                                new Node(nugat_.CONS,
                                                        buchiNodes.firstElement(),
                                                        new Node(Pointer.NULL,nugat_),
                                                        nugat_),
                    nugat_);
            buchiNodes.remove(0);
            buchiNodes.remove(0);
            Iterator iter = buchiNodes.iterator();

            while (iter.hasNext()){
                buchiNode = new Node (nugat_.CONS, (Node)iter.next() ,buchiNode,nugat_);
            }
        }
        
        return buchiNode;
    }

    private Vector<Formula> CompleteBuchiGame(Formula formula) throws IOException{
        BuchiGameIterator iterator = new BuchiGameIterator(formula);
        Vector<Formula> struct = new Vector<Formula>();
        while (iterator.hasNext()){
            struct.add(iterator.getBuchiFormula());
            iterator.next();
        }
        struct.add(iterator.getBuchiFormula());
        return struct;
    }
    
    private Vector<Formula> inverse(Vector<Formula> vector){
        Vector<Formula> newVector = new Vector<Formula>();
        
        for (int i = vector.size()-1; i >= 0; --i){
            newVector.add(vector.get(i));
        }
        
        return newVector;
    }
    
    private Vector<Node> formulaToNode(Vector<Formula> formulae) throws IOException{
        Vector<Node> nodes = new Vector<Node>();
        
        Iterator iter = formulae.iterator();
        while(iter.hasNext()){
            nodes.add(((Formula)iter.next()).encFormula(nugat_, smvTable_));
        }
        
        return nodes;
    }

}
